%-----------------> REWRITE METHOD BODIES
change_methodbodycount(BC, NewBC) :-
	NewBC is BC.

change_methodbodyinfo(MBs, MarkedList, CP, NewMBs, NewMarkedList) :-
	b_setval(jumptable,[]),
	add_sec_var_instructions(MBs,CP,MarkedList,TempMBs,TempMarkedList),

	%	break,
	b_getval(jumptable,JumpTablePrime),
%	format('Jumptable = ~w----------------------------->~n~n', [JumpTablePrime]),
	
	b_getval(securitysize,SecSize),
	correct_jump_table(JumpTablePrime,SecSize,JumpTable),

	%format('New Jump Table after secsize correction~w~n~n', [JumpTable]),
	correct_jump_targets(JumpTable,TempMBs,NewMBs),
	%	format('InstrIndex == ~w~n~n',[InstrIndex]),
	
%	open('beforecorrection.txt','write',TStream),
%	tell(TStream),
%	print_method_bodies(TempMBs),
%	told,

	correct_marked_lists(JumpTable,NewMBs,TempMarkedList,NewMarkedList).

	%	writeln(NewMarkedList),
%	open('rewrittenmethods.txt','write',Stream),
%	tell(Stream),
%	print_method_bodies(NewMBs),
%	told.


correct_jump_table([(Method1,JumpList1)|Rest],SecSize,[(Method1,NewJumpList1)|NewRest]) :-
	reverse(JumpList1,RJumpList1),
	correct_jumplist(RJumpList1,RJumpList1,SecSize,RNewJumpList1),
	reverse(RNewJumpList1,NewJumpList1),
	correct_jump_table(Rest,SecSize,NewRest).
correct_jump_table([],_,[]).

correct_jumplist([(JO,Size)|Rest],CompleteJL,SecSize,[NewElem|NewRest]) :-
	nth(N,CompleteJL,(JO,Size)),
	
	NewJO is (JO + (SecSize * (N - 1))),
	
%	format('N=~w, NewSize=~w~n~n', [N,NewJO]),
	NewElem = (NewJO,Size),
	correct_jumplist(Rest,CompleteJL,SecSize,NewRest).
correct_jumplist([],_,_,[]).
%==================================================== MARKED LIST UPDATE =======
correct_marked_lists(JumpTable,[UnmarkedMB1|UnmarkedRest],[T1|Rest],[T1|NewRest]) :-
	UnmarkedMB1 =.. UnmarkedMB1List,
	nth(2, UnmarkedMB1List, MethodNum),

	get_method_jumplist(JumpTable,MethodNum,JumpList),
	JumpList = [],
	correct_marked_lists(JumpTable,UnmarkedRest,Rest,NewRest).
correct_marked_lists(JumpTable,[UnmarkedMB1|UnmarkedRest],[T1|Rest],[New1|NewRest]) :-
	UnmarkedMB1 =.. UnmarkedMB1List,
	nth(2, UnmarkedMB1List, MethodNum),

	get_method_jumplist(JumpTable,MethodNum,JumpList),
	JumpList \= [],
	nth(8, UnmarkedMB1List, UnmarkedC),
	correct_marked_code(UnmarkedC,T1,New1),
	correct_marked_lists(JumpTable,UnmarkedRest,Rest,NewRest).
correct_marked_lists(_JumpTable,[],[],[]).

correct_marked_code([(_UO - UI)|UC],[(TO - TI,Marking)|TC],[(NO - NI,Marking)|NC]) :-
	%	writeln('Hello1'),
	UI =.. [H|_Args],
	\+is_jump(H),
	correct_marked_code(UC,TC,NC),
	NO is TO,
	NI = TI.
correct_marked_code([(_UO - UI)|UC],[(TO - _TI,Marking)|TC],[(NO - NI,Marking)|NC]) :-
	%writeln('Hello2'),
	UI =.. [H|_Args],
	is_jump(H),
	correct_marked_code(UC,TC,NC),
	%	writeln(H),
	NO is TO,
	NI = UI.
correct_marked_code(_UnmarkedC,[],[]).

%=================================================== CORRECT JUMPT TARGETS ==========
%TODO: right now, not handling negative branches
correct_jump_targets(JumpTable, [MB1|Rest], [NewMB1|NewRest]) :-
	MB1 =.. MB1List,
	nth(2, MB1List, MethodNum),
	get_method_jumplist(JumpTable,MethodNum,JumpList),

	((JumpList = []) -> 	(%Method does not have any jumps
			     	 correct_jump_targets(JumpTable,Rest,NewRest),
			    	 NewMB1 = MB1);
			    	(correct_jumps_single_method(JumpList,MB1,NewMB1),
				 correct_jump_targets(JumpTable,Rest,NewRest))).
correct_jump_targets(_JumpTable, [], []).

correct_jumps_single_method(JumpList,MB,NewMB) :-
	MB =.. [method_body, Method, MS, LC, ISD, MSD, CL, C, EC, E, TC, T],
	correct_jumps_code(JumpList,C,NewC),
	NewMB =.. [method_body, Method, MS, LC, ISD, MSD, CL, NewC, EC, E, TC, T].

correct_jumps_code(JumpList,[O - I|Rest],[O - I|NewRest]) :-
	I =.. [H|Args],
	\+is_jump(H),
	%	writeln('CJC case #1'),
	%	writeln(O - I),
	correct_jumps_code(JumpList,Rest,NewRest).
/* case when the jump offset lands in a place before any security relevant instrs have been added */
correct_jumps_code(JumpList,[O - I|Rest],[O - I|NewRest]) :-
	I =.. [H|Args],
	is_jump(H),
	reverse(JumpList,[(JO,Size)|CorrectedJumpList]),
	I =.. [_Head,JumpOffset],
	Sum is O + JumpOffset + 4,
	Sum =< JO,
	%	find_place_in_jumplist(Sum,[(JO,Size)|CorrectedJumpList],0,Place),
	%writeln('CJC case #2 ------------------------->>>>'),
	%writeln(O - I),
	%format('Place = ~w~n', [Place]),
	correct_jumps_code(JumpList,Rest,NewRest).
correct_jumps_code(JumpList,[O - I|Rest],[O - NewI|NewRest]) :-
	I =.. [H|JumpOffset],
	is_jump(H),
	reverse(JumpList,[(JO,Size)|CorrectedJumpList]),
	Sum is O + JumpOffset + 4,
	Sum > JO,
%	writeln('CJC case #3-------------------------------->>>>'),
%	format('O is ~w, Sum is ~w~n',[O,Sum]),
	find_place_in_jumplist(O,[(JO,Size)|CorrectedJumpList],0,OPlace),
	find_place_in_jumplist(Sum,[(JO,Size)|CorrectedJumpList],0,SumPlace),

%		format('OPlace = ~w, SumPlace = ~w~n',[OPlace, SumPlace]),

	find_total_offset_sum([(JO,Size)|CorrectedJumpList],OPlace,SumPlace,TotalOffsetSum),
	NewJumpOffset is JumpOffset + TotalOffsetSum,
	NewI =.. [H,NewJumpOffset],
%	format('O =~w NewI = ~w~n',[O,NewI]),
%	writeln('------------------------------------------end'),
	%writeln(O - I),
	correct_jumps_code(JumpList,Rest,NewRest).
correct_jumps_code(_JumpList,[],[]).

find_place_in_jumplist(Sum,[(JO,_)|_JumpList],OldPlace,OldPlace) :-
	Sum < JO.
find_place_in_jumplist(Sum,[(JO,_)|JumpList],OldPlace,NewPlace) :-
	Sum >= JO,
	TempPlace is OldPlace + 1,
	find_place_in_jumplist(Sum,JumpList,TempPlace,NewPlace).
find_place_in_jumplist(_Sum,[],OldPlace,NewPlace) :-
	NewPlace is OldPlace.

find_total_offset_sum(JumpList,OPlace,SumPlace,TOS) :-
	sum_till_place(JumpList,OPlace,OTotalSum),
	sum_till_place(JumpList,SumPlace,SumTotalSum),
%		format('OTS is ~w, STS is ~w~n~n', [OTotalSum,SumTotalSum]),
	%	break,
	TOS is SumTotalSum - OTotalSum.

sum_till_place([(JO1,Size1)|Rest],Place,NewTOS) :-
	Place >= 1,
	NewPlace is Place - 1,
	sum_till_place([(JO1,Size1)|Rest],NewPlace,TempTOS),
	NewTOS is TempTOS + Size1.
sum_till_place(_JumpList,0,0).
	
%=====================================================================================
add_sec_var_instructions(MBs, CP, MarkedList, NewMBs, NewMarkedList) :- 

	find_index_multinameCP('gotoAndPlay', CP, InstrIndex),

	b_setval(instrindices,[InstrIndex]),
	
	find_index_multinameCP('nativeApplication', CP, NativeAppIndex),
	b_setval(nativeappindex,NativeAppIndex),
	find_index_multinameCP('exit', CP, HaltIndex),
	b_setval(haltindex,HaltIndex),
	find_index_multinameCP('isOkay',CP,SecVarIndex),

	format('InstrIndex == ~w~n',[InstrIndex]),
	%open('out.txt','write',Stream),
	%tell(Stream),
	
	%abc_parser:getABC(method_bodies,T,MethodBodies),
	%format('UntrustedMethodBodies is ~w~n', [UMethodBodies]),
	%print_method_bodies(MBs),
	%
	%told.
	
	%change_first_method(MBs, CP, SecVarIndex, MarkedList, TempMBs, TempMarkedList),
	TempMBs = MBs,
	TempMarkedList = MarkedList,
	insert_guards_overall(TempMBs, InstrIndex, SecVarIndex, HaltIndex, NativeAppIndex, TempMarkedList, NewMBs, NewMarkedList).
	

%	NewMBs = MBs,
%	NewMarkedList = MarkedList.


change_first_method(MBs, _CP, SecVarIndex, MarkedList, NewMBs, NewMarkedList) :-
	reverse(MBs,[R1|RMBs]),
	R1 =.. [method_body, Method, MS, LC, ISD, MSD, CL, C, EC, E, TC, T],
	

%	writeln('Method Num'),
%	writeln(Method),
		
	%	writeln('last method'),
	%	writeln(C),
	%writeln(CL),

	append(First,[O-returnvoid],C),

	instruction_size(findproperty(SecVarIndex),FSVISize),
	instruction_size(initproperty(SecVarIndex),ISVISize),
	
	O1 is O+FSVISize,
	O2 is O1+2,
	O3 is O2+ISVISize,

	Insert = [O - findproperty(SecVarIndex),
		  O1 - pushbyte(0),
		  O2 - initproperty(SecVarIndex),
		  O3 - returnvoid],

	append(First,Insert,C2),
	
	%	writeln(C2),
	NewCL is CL + FSVISize + 2 + ISVISize,

	%	format('f=~w,i=~w,CL=~w,Newcl=~w~n~n',[FSVISize,ISVISize,CL,NewCL]), 

	R2 =.. [method_body, Method, MS, LC, ISD, MSD, NewCL, C2, EC, E, TC, T],
	TempMBs = [R2|RMBs],
	reverse(TempMBs,NewMBs),

	/* change the marked lists */
	
	reverse(MarkedList,[RM1|RMarkedList]),
	%	writeln('markedlist1'),
	%writeln(RM1),
	append(FirstMarked,[(O-returnvoid,'Unmarked')],RM1),
	
	append(FirstMarked,
		[(O-findproperty(SecVarIndex),'Marked'),
		 (O1-pushbyte(0),'Marked'),
		 (O2-initproperty(SecVarIndex),'Marked'),
	         (O3-returnvoid,'Unmarked')],ChangedRM1),
	reverse([ChangedRM1|RMarkedList],NewMarkedList).

/*	O4 is O + 1,
	InsertTest = [O-nop,O4-returnvoid],

	append(First, InsertTest, CTest),
	writeln(CTest),
	NewCTest is CL + 1,

	NewLC is LC + 1,
	NewMS is MS + 1,
%	R2 =.. [method_body, Method, MS, LC, ISD, MSD, NewCL, C2, EC, E, TC, T],
	

	reverse(MarkedList,[RM1|RMarkedList]),
	writeln('markedlist1'),
	writeln(RM1),
	append(FirstMarked,[(O-returnvoid,'Unmarked')],RM1),
	
	append(FirstMarked,[(O-nop,'Unmarked'),(O4-returnvoid,'Unmarked')],ChangedRM1),
	reverse([ChangedRM1|RMarkedList],NewMarkedList). */


%	NewMarkedList = MarkedList.
%----------------------------------------------------------

%Search through each method body to see if it has the security 
%relevant instruction given by the method name residing at 
%MultinameIndex. Insert guards around that instruction.
%For right now, assuming that the sec rel event is going to be a 
%method call, of the form callpropvoid(index, arg_count). 
%TODO: change insert_instr_method_body to handle other method
%calls such as callproplex(index, arg_count), or callstatic(i, a).
%
%
%TODO: Not sure if setlocal_1 and getlocal_1 are okay to use 
%here. Could there be other values stored in those registers?
%How do we know whether they're free to use?
%
%InstrINdex is the multiname CP index of the security relevant instruction.
%SecVarIndex is the multiname CP index of the security variable.
%HaltIndex is the multiname CP index of the halt method.
insert_guards_overall([MB|MBs], InstrIndex, SecVarIndex, HaltIndex, NativeAppIndex, [MarkedC|MarkedCs], 
			[NewMB|NewMBs], [NewMarkedC|NewMarkedCs]) :- 


	MB =..  [method_body, Method, MS, LC, ISD,
       		MSD, CL, C, EC, E, TC, T],
	
		%writeln('in insert guards overall, Method Num is -------------->'),
		%writeln(Method),
		%writeln('\n\n'),

%	format('NativeAppIndex = ~w, HaltIndex = ~w~n', [NativeAppIndex,HaltIndex]),

	instruction_size(findproperty(NativeAppIndex),S1),
	instruction_size(callpropvoid(HaltIndex,0),S2),
%	instruction_size(pushstring(75),S3),
		
%	format('S1=~w,S2=~w,S3=~w~n',[S1,S2,S3]),
	Sum is S1 + S2,
%	
% break,
%	format('N=~w, H=~w~n', [NativeAppIndex,HaltIndex]),
%	format('SecVarIndex is ~w~n',[SecVarIndex]),
	insert_instr_method_body(Method, C, CL, InstrIndex, [
						
							findproperty(NativeAppIndex),
							callpropvoid(HaltIndex, 0)
							%nop
						], NewC, 0, NewCL, 0, MarkedC, NewMarkedC), 

						%format('New Marked C = ~w~n~n', [NewMarkedC]),				
%	NewLC is LC + 1,
	NewLC is LC + 1,
	NewMS is MS + 1,
%	NewMS is MS + 2,
	NewMB =.. [method_body, Method, NewMS, NewLC, ISD,
       		MSD, NewCL, NewC, EC, E, TC, T],


		
	insert_guards_overall(MBs, InstrIndex, SecVarIndex, HaltIndex, NativeAppIndex, MarkedCs, NewMBs, NewMarkedCs).
insert_guards_overall([], _InstrIndex, _SecVarIndex, _HaltIndex, _NativeAppIndex, MarkedList, [], MarkedList).
%-----------------------------------------------
insert_instr_method_body(MethodNum, [Offset - I|Rest], CL, MultinameIndex, InstrsToInsert,
			   	NewC, OldAddOffset, NewCL, 0,
			       	[_MarkedCodePoint|MarkedCodePoints], 
				NewMarkedCodePoints) :-
	% Check if it's the correct instruction and args.				
	I =.. [Head1, Head2|_Tail],
	Head1 = callpropvoid,
	Head2 = MultinameIndex,

	%	format('I is ~w~n~n', [I]),
	
	% Create the new front part of Instr Array
	create_oi_array(InstrsToInsert, Offset, Front, 0, SumSize, NewInstrMarks),

	% Manipulate the offsets correctly.
	NewAddOffset is OldAddOffset + SumSize,

	%Set everything in the jump table 
	b_getval(jumptable, JumpTable),
	get_method_jumplist(JumpTable,MethodNum,MethodJumpList),

%	format('In IIMB, SumSize = ~w~n~n~n',[SumSize]),
	b_setval(securitysize,SumSize),
	set_method_jumplist(JumpTable,MethodNum,[(Offset,SumSize)|MethodJumpList],NewJumpTable),
%	format('MJL = ~w, NewJumpTable = ~w~n~n', [MethodJumpList,NewJumpTable]),
	b_setval(jumptable, NewJumpTable),

	% Find out the length of the old Instr	
	instruction_size(I, CLInstr),
	RestCL is CL - CLInstr,
%	%---------------- debugging
%	writeln('case 1 of IIMB ----------------------------------------->'),
%	format('Array = ~w~n~n InstrsToInstr = ~w~n~n', [[Offset - I|Rest],InstrsToInsert]),
	%---------------------------

	% Recursively call
	insert_instr_method_body(MethodNum, Rest, RestCL, MultinameIndex, InstrsToInsert, NewRest, 
				 NewAddOffset, NewRestCL, 0, MarkedCodePoints, TempMarkedCodePoints),

	%----------------------------------------------------------------------
	% Pass up the correct NewC
	NewOffset is Offset + SumSize + OldAddOffset,
	%NewOffset is Offset + SumSize,
	Front = [FrontO - FrontI| FrontRest],
	NewFrontO is FrontO + OldAddOffset,


	reset_offsets(NewFrontO,[FrontO - FrontI|FrontRest],ResetList),


%	append([NewFrontO - FrontI|FrontRest], [NewOffset - I], NewFront),
	append(ResetList,[NewOffset-I],NewFront),
	append(NewFront, NewRest, NewC),

%	format('NewC is ~w~n~n',[NewC]),
%	format('NewOffset is ~w, Offset=~w, SumSize=~w, OldAddOffset=~w~n~n',[NewOffset,Offset,SumSize,OldAddOffset]),
%	format('Offset = ~w, NewFrontO=~w, Fronto=~w, OldAddOffset=~w~n~n', [Offset, NewFrontO, FrontO, OldAddOffset]),

	%=============================== Marked Lists ======================================

	NewInstrMarks = [(FrontO - FrontI, 'Marked')|MarkedRest],

	append([(NewFrontO - FrontI,'Marked')|MarkedRest],[(NewOffset - I,'Unmarked')],UpdatedInstrMarks),
	% append the correct Marked lists


	instruction_size(I,ISize),
	FirstMarkedOffset is NewOffset + ISize,
	reset_offsets_in_marked_lists(FirstMarkedOffset,TempMarkedCodePoints,ResetMarkedCodePoints), 
	append(UpdatedInstrMarks, ResetMarkedCodePoints, NewMarkedCodePoints1), 

	%	format('NewMarked = ~w~n~n',[NewMarkedCodePoints1]),
	%	format('after---------------------------------------------------------'),
	
		correct_halt_instr(NewMarkedCodePoints1,NewMarkedCodePoints),

	%	NewMarkedCodePoints = NewMarkedCodePoints1,
	%======================================================================================
	%format('NewMarkedCodePoints are ~w~n',[NewMarkedCodePoints]),

	% Pass up the correct CL
	NewCL is NewRestCL + CLInstr + SumSize.

insert_instr_method_body(MethodNum, [Offset - I|Rest], CL, MultinameIndex, InstrsToInsert,
				[NewOffset - I|NewRest], OldAddOffset, NewCL, Flag,
				[MarkedCodePoint|MarkedCodePoints], 
				[NewMarkedCodePoint|NewMarkedCodePoints]) :-
		% Check if it's the correct instruction and args.
		%writeln(Offset - I),		
	I =.. [Head1, Head2|_Tail],
	Head1 = callpropvoid,
	Head2 \= MultinameIndex,

	%format('I is ~w~n~n', [I]),
	% Manipulate the offsets correctly.
	NewOffset is Offset + OldAddOffset,
	NewAddOffset is OldAddOffset,

	% Find out the length of the Instr
	instruction_size(I, CLInstr),
	%	format('in IIMB, I=~w, CLInstr=~w~n',[I,CLInstr]),

	RestCL is CL - CLInstr,
		
	% Recursively call
	insert_instr_method_body(MethodNum, Rest, RestCL, MultinameIndex, InstrsToInsert, NewRest, 
	                         NewAddOffset, NewRestCL, Flag,
				 MarkedCodePoints, NewMarkedCodePoints),

	NewMarkedCodePoint = MarkedCodePoint,
	% Pass up the correct CL
	NewCL is NewRestCL + CLInstr.

insert_instr_method_body(MethodNum, [Offset - I|Rest], CL, MultinameIndex, InstrsToInsert,
				[NewOffset - I|NewRest], OldAddOffset, NewCL, Flag,
				[MarkedCodePoint|MarkedCodePoints], 
				[NewMarkedCodePoint|NewMarkedCodePoints]) :-			

	I =.. [Head|_Tail],	
	Head \= callpropvoid,	

	%format('I is ~w~n~n', [I]),
	% Manipulate the offsets correctly.
	NewOffset is Offset + OldAddOffset,
	NewAddOffset is OldAddOffset,

	% Find out the length of the Instr
	instruction_size(I, CLInstr),

	RestCL is CL - CLInstr,
		
	% Recursively call
	insert_instr_method_body(MethodNum, Rest, RestCL, MultinameIndex, InstrsToInsert, NewRest,
       	                       	 NewAddOffset, NewRestCL, Flag,
			 	 MarkedCodePoints, NewMarkedCodePoints),
	
	NewMarkedCodePoint = MarkedCodePoint,
	% Pass up the correct CL
	%
	NewCL is NewRestCL + CLInstr.

insert_instr_method_body(_MethodNum, [], CL, _MultinameIndex, _InstrsToInsert, [], _AddOffset, CL, _,
MarkedCodePoints, MarkedCodePoints).
	%writeln('case 5').

%-----------------------------------------------------------
create_oi_array([Instr|InstrArray], InitOffset, [InitOffset - Instr|OIArray],
		 OldSumSize, NewSumSize,
	 	 [MarkedCodePoint|MarkedCodePoints]) :-
	instruction_size(Instr, InstrSize),
	NextOffset is InitOffset + InstrSize,
	NextSumSize is OldSumSize + InstrSize,
	MarkedCodePoint = (InitOffset - Instr, 'Marked'),
	create_oi_array(InstrArray, NextOffset, OIArray, NextSumSize, NewSumSize,
			MarkedCodePoints).
create_oi_array([], _OffsetToAdd, [], SumSize, SumSize, []).

reset_offsets(FirstOffset,[_O-I|Rest],ResetList) :-
	instruction_size(I,Size),
	NextOffset is FirstOffset + Size,
	reset_offsets(NextOffset,Rest,NewRest),
	ResetList = [FirstOffset - I|NewRest].
reset_offsets(_FirstOffset,[],[]).

reset_offsets_in_marked_lists(FirstOffset,[(_O2-I2,Marking)|Rest],NewMarkedCodePoints) :-

	instruction_size(I2,I2Size),
	NextOffset is FirstOffset + I2Size, 
	reset_offsets_in_marked_lists(NextOffset,Rest,NewRest),
	NewMarkedCodePoints = [(FirstOffset-I2,Marking)|NewRest].
reset_offsets_in_marked_lists(_FirstOffset,[],[]).
	
get_method_jumplist([(CurrMethodNum,_CurrJumpList)|JumpTable],MethodNum,JumpList) :-
	CurrMethodNum \= MethodNum,
	get_method_jumplist(JumpTable,MethodNum,JumpList).
get_method_jumplist([(MethodNum,JumpList)|_JumpTable],MethodNum,JumpList).
get_method_jumplist([],MethodNum,[]).
	%	format('method ~ws Jumplist not available',[MethodNum]).

set_method_jumplist([(CurrMethodNum,CurrJumpList)|JumpTable],MethodNum,JumpList,NewJumpTable) :-
	CurrMethodNum \= MethodNum,
	set_method_jumplist(JumpTable,MethodNum,JumpList,TempJumpTable),
	NewJumpTable = [(CurrMethodNum,CurrJumpList)|TempJumpTable].
set_method_jumplist([(MethodNum,_OldJumpList)|JumpTable],MethodNum,NewJumpList,NewJumpTable) :-
	NewJumpTable = [(MethodNum,NewJumpList)|JumpTable].
set_method_jumplist([],MethodNum,JumpList,[(MethodNum,JumpList)]).
	%	format('method ~ws Jumplist not available',[MethodNum]).
	%
is_jump(ifeq).
is_jump(iffalse).
is_jump(ifge).
is_jump(ifgt).
is_jump(ifle).
is_jump(iflt).
is_jump(ifnge).
is_jump(ifngt).
is_jump(ifnle).
is_jump(ifnlt).
is_jump(ifne).
is_jump(ifnge).
is_jump(ifstricteq).
is_jump(ifstrictne).
is_jump(iftrue).
is_jump(jump).

correct_halt_instr([First|Rest],[NewFirst|NewRest]) :-
	b_getval(nativeappindex,NAI),
	b_getval(haltindex,HI),
	%format('NAI = ~w, HI = ~w~n',[NAI,HI]),
	First = (O - callpropvoid(HI,ArgCount),_Marking),
       	NewMarking = 'Unmarked',
	NewFirst = (O - callpropvoid(HI,ArgCount),NewMarking),
	correct_halt_instr(Rest,NewRest).
correct_halt_instr([First|Rest],[NewFirst|NewRest]) :-
	b_getval(nativeappindex,NAI),
	b_getval(haltindex,HI),
	%format('NAI = ~w, HI = ~w~n',[NAI,HI]),
	First \= (O - callpropvoid(HI,ArgCount),_Marking),
        NewFirst = First,
	correct_halt_instr(Rest,NewRest).
correct_halt_instr([],[]).

